| Definitions | Dsys, t  T, Unit, Type, Id, IdLnk, left+right,  , x:A  B(x),  x:A. B(x), M(i), M.state, locl(a), M.da(a), Feasible(D), f(a), P   Q, outl(x), outr(x), s = t, isl(x),   b,  b, A & B, {x:A| B(x) }, A B, x:A B(x), P & Q,  x:A. B(x), Prop, a in dom(M.pre), source(l), M sends on link l, destination(l),  x.A(x), <a,b>, FairFifo, False, A, AtomFree(T;x), A/x,y. B(x;y), vartype(i;x), valtype(i;a), w.M, Msg(M), type List, w-machine(w;i), let x,y,z = a in t(x;y;z), w-machine-constraint(w), M.dout(l,tg), P  Q,  , d-world-state(D;i), d-comp(D;v;sched;dec), CV(F), 2of(t), 1of(t), Knd,  , lnk(k), a = b, isrcv(k), p  q, i j, M.ds(x), hd(l), w.TA, w.T, kind(a), isnull(a), w-atom-constraint(w), Msg, isrcv(l;a), a(i;t), msg(a), m(i;t), s(i;t).x, mlnk(m), filter(P;l), onlnk(l;mss), nil, stutter-state(s), msg(l;t;v), Msg(da), M.Msg, S  T, d-decl(D;i), M.sends(k,s,v), (x l), Void, xL. P(x), a = b, next-world-state(D;i;s;k;v), P  Q, P Q, #$n, n+m, i=j, n-m, s ~ t, State(ds), Case b of inl(x) s(x) ; inr(y) t(y), if b t else f fi, Action(dec), Top, f(x)?z, True, doact(k;v), x. t(x), null, tag(k), World, val(a), ||as||, queue(l;t), rcv(l,tg), d-world(D;v;sched;dec), a<b, inl(x), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), w-action-dec(TA;M;i), Dec(P), M.init(x)?v, d-partial-world(D;f;t';s), mval(m), mtag(m), i<j, i = j, M.dout2(l;tg), let x = a in b(x), d-comp-partial-world(D;v;sched;dec;t), x,y. t(x;y), inr(x), *,  , true, false, {T},  x:A. B(x), null(as), d-machine(i;M;dec), p q, M.ef(k,x,s,v)?w, SQType(T), act(k),  T, MsgA, -n, S  T, {i..j }, i j < k, Valtype(da;k), tl(l), if a<b c ; d fi, ij, nth_tl(n;as), l[i], a:A fp B(a), "$token", if a=b c ; d fi, NatDeq, atom-deq-aux, if a=bAtomc; d fi, x=yAtom, AtomDeq, IdDeq, IdLnkDeq, prod-deq(A;B;a;b), proddeq(a;b), product-deq(A;B;a;b), Atom, sum-deq(A;B;a;b), sumdeq(a;b), union-deq(A;B;a;b), KindDeq, f(x), eqof(d), Case of a; nil s ; x.y, rec:z t(x;y;z), Y, reduce(f;k;as), deq-member(eq;x;L), x dom(f), ds(M), AtomFree(d), da(M) |
| Lemmas | atom-free-ma-dout, atom-free-ma-da, d-da-atom-free, atom-free-ma-ds, d-ds-atom-free, subtype rel list, subtype rel transitivity, filter type, locl one one, pi2 wf, inr equal, decidable equal Id, IdLnk sq, bnot of lt int, assert of le int, le int wf, ifthenelse wf, d-partial-world wf, int seg wf, ma-init-val wf, squash wf, msga wf, ma-ef-val wf, Id sq, equal-next-world, next-world-state wf, bool sq, Knd sq, islocal wf, w-isnull wf, w-a wf, w-queue-nil, CV wf, d-comp wf2, pos length, assert-d-eq-Loc, w-queue-partial, assert of null, null wf3, top wf, null-action wf, decidable false, btrue wf, bfalse wf, mtag wf, mval wf, assert of lt int, w-queue-wf2, action wf, doact wf, kindcase wf, ma-dout2 wf, rcv wf, d-eq-Loc wf, lt int wf, d-comp-partial-world wf, decidable assert, inr eq inl, d-world wf, ge wf, length wf1, hd wf, w-queue wf, w-Msg wf, tagof wf, pi1 wf, d-decl wf, Knd wf, d-world-state wf, true wf, false wf, d-msg-subtype, member wf, ma-ds wf, eqtt to assert, eqff to assert, assert of bnot, assert of eq int, eq int wf, bool wf, not functionality wrt iff, iff transitivity, assert of band, and functionality wrt iff, assert-eq-lnk, assert-eq-id, filter filter, filter is nil, eq id wf, l member wf, ma-send-val wf, d-decl-subtype2, ma-msg wf, mlnk wf d, msg wf, subtype rel self, filter wf, mlnk wf, Msg wf, ma-dout wf, not wf, band wf, isrcv wf, eq lnk wf, lnk wf, nat properties, better-d-comp-step, ldst wf, ma-sends-on wf, lsrc wf, ma-has-pre wf, le wf, assert wf, bnot wf, isl wf, outr wf, outl wf, d-feasible wf, ma-da wf, locl wf, ma-st wf, d-m wf, nat wf, IdLnk wf, Id wf, unit wf, dsys wf |
dec:(j,b:Id